"""
    Copyright (C) 2007, 2008 Sasa Petrovic

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU Lesser General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU Lesser General Public License for more details.

    You should have received a copy of the GNU Lesser General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
"""


import types, itertools

#this is the class variable
class variable(object):
    #to initialize a variable you pass the name as the parameter
    def __init__(self, name):
        self.name = name
    
    #to check whether two variables are equal you pass one referenced to the other example: var1 == var2
    def __eq__(self, other):#returns true if they both have the same name, false otherwise
        if isinstance(other, variable):
            return self.name == other.name
        else:
            return False
        
    def __repr__(self):#returns the name if its being printed
        return self.name

    def __iter__(self):#returns the iter([]) 
        return iter([])

#the constant class -----> Same explanation as that for variable class but for constant
class constant(object):
    def __init__(self, content):
        self.content = content
        
    def __eq__(self, other):
        if isinstance(other, constant):
            return self.content == other.content
        else:
            return False
        
    def __iter__(self):
        return iter([])
    
    def __repr__(self):
        return self.content

#the function class -----> Same explanation as that for variable class but for function
class function(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, function):
            return self.name == other.name
        else:
            return False
    
    def __repr__(self):
        return self.name
    
    def __iter__(self):
        return iter([])

#the predicate class -----> Same explanation as that for variable class but for predicate
class predicate(object):
    def __init__(self, name):
        self.name = name
        
    def __eq__(self, other):
        if isinstance(other, predicate):
            return self.name == other.name
        else:
            return False
    
    def __repr__(self):
        return self.name
    
    def __iter__(self):
        return iter([])

class substitution(object):
    def __init__(self, first = None, second = None):#the first and second could be not passed
        #print 'in init in substitution' #in the init we initialize the substitutions 
        if first and second:#if the first and second are not empty, then the second must be a variable
            #so we initialize the substitutions such that the variable is the second 
            #element in the pair since the second pair would be the bottom of the unifier
            self.substitutions = [(first, second)]
        else:
            #if one of the parameters passed is empty then initialize self.substitutions to an empty set
            self.substitutions = []
        #print 'the sub is',self.substitutions
    
    #this method returns the correct numerator of a unifier according to the parameters sent
    #parameters are what a variable can be unified to, as well as a pair one of which a variable and the other
    #would be its unifier (substitution)
    def resolve(self, leftList, other):
        #print 'in resolve'
        #print other,'other'
        #print leftList,'leftList'
        f, s = other#this assigns f to the 1st value in the pair passed and s the 2nd
        #f is the above value of the unifier other
        #s is the below value of the unifier other (the variable)
        #print 'f & s',f,s
        result = []#initialize result which will be updated according to the following code
        if isinstance(leftList, (variable, constant, function, predicate)):
            #if the leftList is a function, variable, constant or predicate, then it
            #does not need to be changed and so we return it right away to be appended to our final result
            return leftList
        if not leftList:#if the leftList is empty 
            return []#then the return should be an empty value as well
        #because there is no unifier available for an empty set with any set
        if isinstance(leftList[0], types.ListType):
            #if the leftList's first value is still of type list
            #print 'leftList is ListType',leftList
            #then it should be furtherly resolved and append the result of resolving it
            #to the current result to preserve the order of the returned result
            result.append(self.resolve(leftList[0], other))
            #print result
        else:
            #the leftList is a numerator not a list ex [a,[f,x]] ex [a]
            #print leftList[0],'else'
            #if the passed numerator is the same as the denominator of the 'other' 
            #substitution that is passed
            #meaning that there do exist a unifier for the corresponding variable 
            #simpler than the already stored one
            if leftList[0] == s:
                #print 'leftList = s'
                #this means that the numerator should be the updated value in the other
                #which is f and hence we append it to the final result
                result.append(f)
            else:
                #print 'leftList is not equal s'
                #if however they are not equal then we should consider the leftList 
                #and append it to the final result since it cannot be unified further 
                #using the passed pair 
                result.append(leftList[0])
        #at this point, we have stored the possible further unifications that can be done
        #using the passed pair of substitution (unifier) on the first element in the leftList
        #we need to recursively call self.resolve on the remaining elements in leftList other than 
        #leftList[0] and extend the current result with the result out of the resursive call
        result.extend(self.resolve(leftList[1:], other))
        #print result,'BEFORE LOOP'
        result = [i for i in result if i]
        #print 'last in resolve'
        #print result
        return result
    
    
    #called when the instance is called as a function ex alpha(beta) or alpha(list)
    def __call__(self, other,flag):
        self.flag = flag
        #print 'in call other is ', other
        #the other is either called as a substitution in alpha(beta) or as a list in alpha(tail(k1)) and alpha(tail(k2))
        if isinstance(other, substitution):#if the passed argument is a substitution then we can start
            #looping on those elements and start resolving both self.substitutions and other.substitutions
            #together 
            # add new substitution 
            if other.substitutions:#just to make sure that the other.substitutions is not empty
                #ex if beta has substitutions 
                #print ' other substitutions not empty'
                #print other.substitutions
                for j in xrange(len(other.substitutions)):#ex loop on beta's substitutions
                    #j is the index in other.substitutions that'll be used
                    #print 'in call - in outer loop'
                    for i in xrange(len(self.substitutions)):#ex loop on alpha's substitutions
                        #i is the index in self.substitutions (referenced variables' substitution index)
                        #print 'in call - in inner loop'
                        #we compare each unified element in alpha with all the unifiers in
                        #beta to make sure we get the best unified output with the corresponding variable
                        #in alpha which is in the second position in its' substitutions list of pairs
                        self.substitutions[i] = (self.resolve(self.substitutions[i][0],\
                                                              other.substitutions[j]),\
                                                              self.substitutions[i][1])
                        #if self.substitutions[i][0] == other.substitutions[j][1]:
                            #self.substitutions[i] = (other.substitutions[j][0], self.substitutions[i][1])
                        #if the variable to be unified in the self.substitutions is the same as the one in other.substitutions
                        #then we should replace the second element in the pair at position i in self.substitutions
                        #with the first element in other.substitutions because we already compared to get the first 
                        #element in the pair in self.resolve
                        if self.substitutions[i][1] == other.substitutions[j][1]:
                            #print 'in call, in if, after loop, substitutions i = j'
                            self.substitutions[i] = (self.substitutions[i][0], other.substitutions[j][0])
                    #At this point we have compared the jth element in the other.substitutions and we no longer will compare it again
                    #so now we can store it in self.substitutions and append that element to self.substitutions and continue to compare all the other.substitutions
                    #with all the elements in self.substitutions including the ones we append
                    self.substitutions.append(other.substitutions[j])
            return self #return this substitution with the self.substitutions edited
        elif isinstance(other, types.ListType):
            #if other is not a substitution, but is a list then we should do the following
            #print 'else - type of other = list type'
            # replace every occurrence of second by first
            new = []#instantiate an empty list of substitutions
            #print other,'other'
            for element in other:#loop on the 'other' list element by element
                #print 'loop element in other'
                #print element, 'Element'
                #if element is a variable (x,y,z..) then we should loop on the substitutions to try to find 
                #a replacement for that variable and hence append 
                if isinstance(element, variable):# 1) if the element is a variable then we
                    #print 'element is variable'
                    rplc = False#a temporary boolean variable to store whether a replacement has been done or not
                    for s in self.substitutions:
                        # 2) should loop on the substitutions instance list and check if that variable
                        #print 's in substitutions'
                        if s[1] == element:
                            # 3) is being used. If so then we should replace it in the substitutions list
                            #print 's[1] = element',s[1]
                            new.append(s[0])# 4) with the 1st value in the same substitution (the top of the inference rule)
                            rplc = True #switch the boolean replacement variable to true
                        #the replacement is not changed in the substitutions list right away, it is
                        #done in the 'new' substitutions list and then that list is returned from the method
                        # the substitutions list is updated when the passed list is
                        #already an instance of the inferred one
                    if not rplc:#if no replacement was done
                        #print 'not rplc',element
                        new.append(element)#then just append that variable to the new 
                elif isinstance(element, types.ListType):#if the element is a list
                    #print 'element is list type'
                    new.append(self.__call__(element,flag))#perform a recursive call to the call method on that list
                    #and append it so that the final 'new' result is in the correct order
                else:#if its a function, predicate or constant, 
                    #then logically we should just append that element to the 'new' substitution list
                    #because only a variable that can be replaced using the substitutions list
                    #that already exist in the instanced substitution
                    new.append(element)
                    #print 'element append'
            #print 'current new' , new
            return new #by that we would have all the elements in the passed list checked
            #and updated according to the substitutions list and so we should return 
            #the 'new' list now.
        else:
            pass
        
    def __repr__(self):#this is where we #print our substitution 
        ##print 'in repr'
        if not self.substitutions:#check if the substitutions is empty
        #    #print 'no substitutions'#if it is empty #print so and return an empty set string
            return '{}'
        s = '{'#if reached here then there are values in the substitution set
        #and now we created a string with the open curly brackets
        for i in self.substitutions:#loop on the substitutions list
            s += '(' + `i[0]` + '/'#and add the open bracket and then the first element
            #which is the top of the inference rule
            #concatenated with the / and the second element; the bottom of the inference rule
            s += `i[1]` +'), ' # and then close that bracket again
        #then we #print the resulted string
        ##print s
        ##print s[:-2] 
        return s[:-2] + '}'
    
#the error class 
class error(object):
    def __init__(self, msg):#here we initialize the self.message to the passed argument
        self.message = msg
        
    def __repr__(self):#here we return a string specifying that there is an error
        return "error: %s" % self.message#along with the error message
    
#this method takes as a parameter a list
def head(ls):
    if not ls:#if the list is empty then the first element of it is None 
        return None #as shown in the return
    return ls[0] # else this method will return the 1st element in the list (indexed 0)

#this method takes as a parameter a list
def tail(ls):
    return ls[1:]#and returns all the list without only the 1st element (starting from index 1)

def mgUnifier(k1, k2,flag):
    """Return the most general unifier of two expressions k1 and k2."""
    #print 'in mgUnifier'
    #print k1, k2
    if not k1 or not k2:#checks if any of the terms is empty
        ##print 'k1 and k2 are none'
        #if one of the terms is empty then we'll return an empty substitution
        #for this specific pair
        return substitution()
    #if any of the terms k1 or k2 are constants, variables, functions or predicates, we should visit this if condition
    #otherwise we will have to recursively call mgUnifier on the heads of the parameters
    #until this if condition is true
    #since getting the unification of any two FOL terms means comparing any functions,constants,variables or predicates with each other
    #in the terms, then we will do so by recursively calling mgUnifier of the heads of the terms
    #until we reach a term comparable to use to get our substitution (unifier)
    if isinstance(k1, (constant, variable, function, predicate)) or isinstance(k2, (constant, variable, function, predicate)):
        if k1 == k2:
        #if k1 & k2 are both constants, variables, functions or predicates
        #then we should call substitution and return an empty set because
            #if this is the case no unifier can be put in our
            ##print 'k1 == k2'
            return substitution()#final substitution for those pairs
        #if we assume that both k1 and k2 are two of those (ex a and a or P and P or x and x or f and f)
        #the pairs cannot produce a unifier together so we call substitution() to return an empty []
        if isinstance(k1, variable):#if the 1st term k1 is a variable
            ##print 'k1 is variable',k1,k2
            if k1 in k2:#and that variable is being used in k2 (its in k2)
                #print 'k1 in k2'
                return error(`k1` + " in " + `k2`)#we should return an error 
            #because you can't unify a variable with a term that has this variable part of it
            else:
                #if the variable is not in the term then we can create a pair such that the variable
                #k1 unifies to the term k2
                return substitution(k2, k1)
        #this condition checks the same as the previous one but with k2 as the variable and k1 as the term to be unified to
        if isinstance(k2, variable):#the same condition for k1 but for k2; if the 2nd term k2 is a variable
            #print 'k2 is variable'
            if k2 in k1:#and that variable is being used in k1 (its in k1)
                #print 'k2 in k1'
                return error(`k2` + " in " + `k1`)#we should return an error
            else:
                return substitution(k1, k2)
        # not convinced with this if
        # if they are both not variables; hence, one of them is either constants, functions or predicates; then they cannot be unified
        if not isinstance(k1, variable) and not isinstance(k2, variable):
            #print 'k1 and k2 are not variables'
            return error(`k1` + " and " + `k2` + " cannot be unified!")#return that the error is that they cannot be unified
    #get the unifier of the heads of both terms and assign alpha to it
    alpha = mgUnifier(head(k1), head(k2),flag)
    if flag and not alpha == '{}':
        print '**************************************'
        print k1, ' and ', k2
        print alpha
    if isinstance(alpha, error):#if the return of calling the mgUnifier for the heads of
        #the heads cannot be unified, then the whole term cannot be unified and return error
        return alpha
    #if reached this line then the heads were unified successfully
    #and what's left is unifying the tails as well
    #k3 and k4 call the __call__(other) method
    #alpha is the unifier substitution for the heads of k1 and k2
    k3 = alpha(tail(k1),flag) #assign variable k3 to the tail of k1
    k4 = alpha(tail(k2),flag) #assign variable k4 to the tail of k2
    #k3 is the substitutions for the tail(k1) comparing the unifier resulted from the heads of k1 and k2
    #with the tails of k1
    #k4 same but with the tails of k2
    #print k3, k4 
    #print 'create beta'
    #this will result with k3 and k4 replacing the tails of k1 and k2 with the unifier resulted from
    #k1 and k2's heads respectively
    beta = mgUnifier(k3, k4,flag)#Now we can call mgUnifier on the resulted most unified so far 
    #values of k3 and k4 using k1 and k2's heads unified together
    if isinstance(beta, error):#check if the tail returned an error and couldn't be unified
        return beta#return that error as well
    #print 'alpha in beta'
    #alpha(beta) is calling __call__(other) in the substitution class
    return alpha(beta,flag)

def main():
    P = predicate("P")#instantiate a predicate P
    g = function("g")#declare that g is a function
    f = function("f")#declare that f is a function
    x = variable("x")#declare that x is a variable
    u = variable("u")
    v = variable("v")
    y = variable("y")#declare that y is a variable
    z = variable("w")#declare that w is a variable
    a = constant("a")#declare that a is a constant
    print '---------------------------------------------------------------------------'
    print 'Test Case 1'
    k1= [P, x, [g, x], [g, [f , a]]]#the first FOL term
    k2= [P, [f , u], v , v]#the second FOL term
    print 'input = ',k1,' and ', k2
    flag = True
    if flag:
        print 'Trace Mode'
        print '-----------'
    uni = mgUnifier(k1, k2,flag)#the MGU, if one exists
    print uni
    print '___________________________________________________________________________'
    flag = False
    if not flag:
        print 'Regular Mode'
        print '--------------'
    uni = mgUnifier(k1,k2,flag)
    print uni
    print '---------------------------------------------------------------------------'
    print 'Test Case 2'
    k1 = [P, a, y, [f, y]]
    k2 = [P, z, z, u]
    print 'input = ',k1,' and ', k2
    flag = True
    if flag:
        print 'Trace Mode'
        print '-----------'
    uni = mgUnifier(k1, k2,flag)#the MGU, if one exists
    print uni
    print '___________________________________________________________________________'
    flag = False
    if not flag:
        print 'Regular Mode'
        print '--------------'
    uni = mgUnifier(k1,k2,flag)
    print uni
    print '---------------------------------------------------------------------------'
    print 'Test Case 3'
    k1 = [f,x,[g,x],x]
    k2 = [f,[g,u],[g,[g,z]],z]
    print 'input = ',k1,' and ', k2
    flag = True
    if flag:
        print 'Trace Mode'
        print '-----------'
    uni = mgUnifier(k1, k2,flag)#the MGU, if one exists
    print uni
    print '___________________________________________________________________________'
    flag = False
    if not flag:
        print 'Regular Mode'
        print '--------------'
    uni = mgUnifier(k1,k2,flag)
    print uni

if __name__ == "__main__":#the call for the main function
    main()